if $p$:$P$ then $A$($p$) else $B$ fi $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $d$ of inl($p$) =$>$ $A$($p$) $\mid$ inr($x$) =$>$ $B$